1. Field of the Invention
The present invention relates in general to verifying designs and in particular to verifying a logic function using a decision diagram. Still more particularly, the present invention relates to a system, method and computer program product for case-splitting on nodes in a symbolic simulation framework.
2. Description of the Related Art
Formal and semiformal verification techniques provide powerful tools for discovering errors in verifying the correctness of logic designs. Formal and semiformal verification techniques frequently expose probabilistically uncommon scenarios that may result in a functional design failure. Frequently, formal and semiformal verification techniques provide the opportunity to prove that a design is correct (i.e., that no failing scenario exists).
One commonly-used approach to formal and semiformal analysis for applications operating on representations of circuit structures is to represent the underlying logical problem structurally (as a circuit graph), and then use Binary Decision Diagrams (BDDs) to convert the structural representation into a functionally canonical form.
In such an approach, in which a logical problem is represented structurally and binary decision diagrams are used to convert the structural representation into a functionally canonical form, a set of nodes for which binary decision diagrams are required to be built, called “sink” nodes, are identified. Examples of sink nodes include the output node or nodes in an equivalence checking or a false-paths analysis context. Examples of sink nodes also include targets in a property-checking or model-checking context.
Unfortunately, formal verification techniques require computational resources which are exponential with respect to the size of the design under test. In particular, many formal analysis techniques require exponential resources with respect to the number of state elements in the design under test. Semi-formal verification techniques leverage formal algorithms on larger designs by applying them only in a resource-bounded manner, though at the expense of incomplete verification coverage; generally, coverage decreases as design size increases.
Symbolic simulation is a symbolic exploration approach that has been used to exhaustively check designs for a bounded number of steps, starting at the initial states. This method verifies a set of scalar tests with a single symbolic vector. Symbolic inputs (represented as BDDs) are assigned to the inputs and propagated through the circuit to the outputs. This technique has the advantage that large input spaces are covered in parallel with a single symbolic sweep of the circuit. Symbolic simulation is resource intensive, however, due to the explosion of BDD representations.